M:MsgA, k:Knd, x:Id. M.frame(k affects x)  Prop 

latex

Definitions	MsgA, M.frame(k affects x), z != f(x)  P(a;z), x,y. t(x;y), IdDeq, Prop, deq-member(eq;x;L), KindDeq, b, x  dom(f), a:A fp B(a), x. t(x), x:A. B(x), Id, t  T, Knd
Lemmas	Knd wf, Id wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, Kind-deq wf, deq-member wf, id-deq wf, fpf-val wf, msga wf